
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">

<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<title>Module ErgoSpec.Common.Types.ErgoTypetoErgoCType</title>
<meta name="description" content="Documentation of Coq module ErgoSpec.Common.Types.ErgoTypetoErgoCType" />
<link href="coq2html.css" rel="stylesheet" type="text/css" />
<script type="text/javascript" src="coq2html.js"> </script>
</head>

<body onload="hideAll('proofscript')">
<h1 class="title">Module ErgoSpec.Common.Types.ErgoTypetoErgoCType</h1>
<div class="coq">
<br/>
<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html">String</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html">List</a></span>.<br/>
<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html">ErgoSpec.Backend.ErgoBackend</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Common.Utils.Misc.html">ErgoSpec.Common.Utils.Misc</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Common.Utils.Names.html">ErgoSpec.Common.Utils.Names</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Common.Utils.Result.html">ErgoSpec.Common.Utils.Result</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html">ErgoSpec.Common.Utils.Provenance</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Common.Utils.Ast.html">ErgoSpec.Common.Utils.Ast</a></span>.<br/>
<span class="kwd">Require</span> <span class="kwd">Import</span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html">ErgoSpec.Common.Types.ErgoType</a></span>.<br/>
<br/>
<span class="kwd">Section</span> <span class="id"><a name="ErgoTypetoErgoCType">ErgoTypetoErgoCType</a></span>.<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="expand_hierarchy">expand_hierarchy</a></span> : <span class="kwd">Set</span> := <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>.<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="expanded_type">expanded_type</a></span> : <span class="kwd">Set</span> := <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> * <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#laergo_type">laergo_type</a></span>).<br/>
&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="expand_ctxt">expand_ctxt</a></span> : <span class="kwd">Set</span> := <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> * (<span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#expand_hierarchy">expand_hierarchy</a></span> * <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#expanded_type">expanded_type</a></span>)).<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Section</span> <span class="id"><a name="ErgoTypetoErgoCType.ErgoTypeExpansion">ErgoTypeExpansion</a></span>.<br/>
<div class="doc">Assumes decls sorted in topological order </div>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="ergo_expand_extends">ergo_expand_extends</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ctxt</span>:<span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#expand_ctxt">expand_ctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">this</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Names.html#absolute_name">absolute_name</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">super</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Names.html#absolute_name">absolute_name</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">localtype</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> * <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#laergo_type">laergo_type</a></span>)) : <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#expand_ctxt">expand_ctxt</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Assoc.html#lookup">lookup</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string_dec">string_dec</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ctxt">ctxt</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#super">super</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> =&gt; <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ctxt">ctxt</a></span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> (<span class="id">hierarchy</span>, <span class="id">etype</span>) =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#this">this</a></span>, (<span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#super">super</a></span>::<span class="id">hierarchy</span>,<span class="id">etype</span> ++ <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#localtype">localtype</a></span>)) :: <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ctxt">ctxt</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="ergo_decl_expand_extends">ergo_decl_expand_extends</a></span> (<span class="id">ctxt</span>:<span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#expand_ctxt">expand_ctxt</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">this</span>:<span class="id"><a href="ErgoSpec.Common.Utils.Names.html#absolute_name">absolute_name</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">decl_desc</span>:<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#laergo_type_declaration_desc">laergo_type_declaration_desc</a></span>) : <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#expand_ctxt">expand_ctxt</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#decl_desc">decl_desc</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeEnum">ErgoTypeEnum</a></span> <span class="id">_</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ctxt">ctxt</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeTransaction">ErgoTypeTransaction</a></span> <span class="id">_</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> <span class="id">rtl</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">if</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string_dec">string_dec</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#this">this</a></span> "<span class="id">org.hyperledger.composer.system.Transaction</span>"%<span class="id">string</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">then</span> (<span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#this">this</a></span>, (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>, <span class="id">rtl</span>)) :: <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ctxt">ctxt</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">else</span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ergo_expand_extends">ergo_expand_extends</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ctxt">ctxt</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#this">this</a></span> "<span class="id">org.hyperledger.composer.system.Transaction</span>"%<span class="id">string</span> <span class="id">rtl</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeTransaction">ErgoTypeTransaction</a></span> <span class="id">_</span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id">super</span>) <span class="id">rtl</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ergo_expand_extends">ergo_expand_extends</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ctxt">ctxt</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#this">this</a></span> <span class="id">super</span> <span class="id">rtl</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeConcept">ErgoTypeConcept</a></span> <span class="id">_</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> <span class="id">rtl</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#this">this</a></span>, (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>, <span class="id">rtl</span>)) :: <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ctxt">ctxt</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeConcept">ErgoTypeConcept</a></span> <span class="id">_</span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id">super</span>) <span class="id">rtl</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ergo_expand_extends">ergo_expand_extends</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ctxt">ctxt</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#this">this</a></span> <span class="id">super</span> <span class="id">rtl</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeEvent">ErgoTypeEvent</a></span> <span class="id">_</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> <span class="id">rtl</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">if</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string_dec">string_dec</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#this">this</a></span> "<span class="id">org.hyperledger.composer.system.Event</span>"%<span class="id">string</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">then</span> (<span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#this">this</a></span>, (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>, <span class="id">rtl</span>)) :: <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ctxt">ctxt</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">else</span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ergo_expand_extends">ergo_expand_extends</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ctxt">ctxt</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#this">this</a></span> "<span class="id">org.hyperledger.composer.system.Event</span>"%<span class="id">string</span> <span class="id">rtl</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeEvent">ErgoTypeEvent</a></span> <span class="id">_</span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id">super</span>) <span class="id">rtl</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ergo_expand_extends">ergo_expand_extends</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ctxt">ctxt</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#this">this</a></span> <span class="id">super</span> <span class="id">rtl</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeAsset">ErgoTypeAsset</a></span> <span class="id">_</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> <span class="id">rtl</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">if</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string_dec">string_dec</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#this">this</a></span> "<span class="id">org.hyperledger.composer.system.Asset</span>"%<span class="id">string</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">then</span> (<span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#this">this</a></span>, (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>, <span class="id">rtl</span>)) :: <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ctxt">ctxt</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">else</span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ergo_expand_extends">ergo_expand_extends</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ctxt">ctxt</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#this">this</a></span> "<span class="id">org.hyperledger.composer.system.Asset</span>"%<span class="id">string</span> <span class="id">rtl</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeAsset">ErgoTypeAsset</a></span> <span class="id">_</span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id">super</span>) <span class="id">rtl</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ergo_expand_extends">ergo_expand_extends</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ctxt">ctxt</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#this">this</a></span> <span class="id">super</span> <span class="id">rtl</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeParticipant">ErgoTypeParticipant</a></span> <span class="id">_</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> <span class="id">rtl</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">if</span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string_dec">string_dec</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#this">this</a></span> "<span class="id">org.hyperledger.composer.system.Participant</span>"%<span class="id">string</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">then</span> (<span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#this">this</a></span>, (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>, <span class="id">rtl</span>)) :: <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ctxt">ctxt</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">else</span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ergo_expand_extends">ergo_expand_extends</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ctxt">ctxt</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#this">this</a></span> "<span class="id">org.hyperledger.composer.system.Participant</span>"%<span class="id">string</span> <span class="id">rtl</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeParticipant">ErgoTypeParticipant</a></span> <span class="id">_</span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id">super</span>) <span class="id">rtl</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ergo_expand_extends">ergo_expand_extends</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ctxt">ctxt</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#this">this</a></span> <span class="id">super</span> <span class="id">rtl</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeGlobal">ErgoTypeGlobal</a></span> <span class="id">_</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ctxt">ctxt</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeFunction">ErgoTypeFunction</a></span> <span class="id">_</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ctxt">ctxt</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeContract">ErgoTypeContract</a></span> <span class="id">_</span> <span class="id">_</span> <span class="id">_</span> =&gt; <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ctxt">ctxt</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Fixpoint</span> <span class="id"><a name="ergo_expand_extends_in_declarations">ergo_expand_extends_in_declarations</a></span> (<span class="id">decls</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#laergo_type_declaration">laergo_type_declaration</a></span>) : <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#expand_ctxt">expand_ctxt</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html#fold_left">List.fold_left</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="kwd">fun</span> <span class="id">ctxt</span> <span class="id">decl</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ergo_decl_expand_extends">ergo_decl_expand_extends</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ctxt">ctxt</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#decl">decl</a></span>.(<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#type_declaration_name">type_declaration_name</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#decl">decl</a></span>.(<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#type_declaration_type">type_declaration_type</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#decls">decls</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="ergo_hierarchy_from_expand">ergo_hierarchy_from_expand</a></span> (<span class="id">ctxt</span> : <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#expand_ctxt">expand_ctxt</a></span>) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html#concat">List.concat</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html#map">List.map</a></span> (<span class="kwd">fun</span> <span class="id">xyz</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html#map">List.map</a></span> (<span class="kwd">fun</span> <span class="id">x</span> =&gt; (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#fst">fst</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#xyz">xyz</a></span>, <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#x">x</a></span>)) (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#fst">fst</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#snd">snd</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#xyz">xyz</a></span>)))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ctxt">ctxt</a></span>).<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">End</span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ErgoTypetoErgoCType.ErgoTypeExpansion">ErgoTypeExpansion</a></span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Section</span> <span class="id"><a name="ErgoTypetoErgoCType.ErgoTypetoErgoCType">ErgoTypetoErgoCType</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Context</span> {<span class="id">m</span>:<span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Brands.BrandRelation.html#brand_relation">brand_relation</a></span>}.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Import</span> <span class="id">ErgoCTypes</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="enums_ctxt">enums_ctxt</a></span> : <span class="kwd">Set</span> := <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Fixpoint</span> <span class="id"><a name="ergo_type_to_ergoc_type">ergo_type_to_ergoc_type</a></span> (<span class="id">t</span>:<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#laergo_type">laergo_type</a></span>) : <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ergoc_type">ergoc_type</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#t">t</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeAny">ErgoTypeAny</a></span> <span class="id">_</span> =&gt; <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.ttop">ttop</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeNothing">ErgoTypeNothing</a></span> <span class="id">_</span> =&gt; <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tbottom">tbottom</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeUnit">ErgoTypeUnit</a></span> <span class="id">_</span> =&gt; <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tunit">tunit</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeBoolean">ErgoTypeBoolean</a></span> <span class="id">_</span> =&gt; <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tbool">tbool</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeString">ErgoTypeString</a></span> <span class="id">_</span> =&gt; <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tstring">tstring</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeDouble">ErgoTypeDouble</a></span> <span class="id">_</span> =&gt; <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tfloat">tfloat</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeLong">ErgoTypeLong</a></span> <span class="id">_</span> =&gt; <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tfloat">tfloat</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeInteger">ErgoTypeInteger</a></span> <span class="id">_</span> =&gt; <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tnat">tnat</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeDateTime">ErgoTypeDateTime</a></span> <span class="id">_</span> =&gt; <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tdateTime">tdateTime</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeClassRef">ErgoTypeClassRef</a></span> <span class="id">_</span> <span class="id">cr</span> =&gt; <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tbrand">tbrand</a></span> (<span class="id">cr</span>::<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeOption">ErgoTypeOption</a></span> <span class="id">_</span> <span class="id">t</span> =&gt; <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.teither">teither</a></span> (<span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ergo_type_to_ergoc_type">ergo_type_to_ergoc_type</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#t">t</a></span>) <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tunit">tunit</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeRecord">ErgoTypeRecord</a></span> <span class="id">_</span> <span class="id">rtl</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.trec">trec</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.open_kind">open_kind</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Bindings.html#rec_sort">rec_sort</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html#map">List.map</a></span> (<span class="kwd">fun</span> <span class="id">xy</span> =&gt; (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#fst">fst</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#xy">xy</a></span>, <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ergo_type_to_ergoc_type">ergo_type_to_ergoc_type</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#snd">snd</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#xy">xy</a></span>))) <span class="id">rtl</span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Bindings.html#rec_sort_sorted">rec_sort_sorted</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html#map">List.map</a></span> (<span class="kwd">fun</span> <span class="id">xy</span> =&gt; (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#fst">fst</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#xy">xy</a></span>, <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ergo_type_to_ergoc_type">ergo_type_to_ergoc_type</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#snd">snd</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#xy">xy</a></span>))) <span class="id">rtl</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Bindings.html#rec_sort">rec_sort</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html#map">List.map</a></span> (<span class="kwd">fun</span> <span class="id">xy</span> =&gt; (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#fst">fst</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#xy">xy</a></span>, <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ergo_type_to_ergoc_type">ergo_type_to_ergoc_type</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#snd">snd</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#xy">xy</a></span>))) <span class="id">rtl</span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Logic.html#eq_refl">eq_refl</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeArray">ErgoTypeArray</a></span> <span class="id">_</span> <span class="id">t</span> =&gt; <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tcoll">tcoll</a></span> (<span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ergo_type_to_ergoc_type">ergo_type_to_ergoc_type</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#t">t</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#ErgoTypeSum">ErgoTypeSum</a></span> <span class="id">_</span> <span class="id">t1</span> <span class="id">t2</span> =&gt; <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.teither">teither</a></span> (<span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ergo_type_to_ergoc_type">ergo_type_to_ergoc_type</a></span> <span class="id">t1</span>) (<span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ergo_type_to_ergoc_type">ergo_type_to_ergoc_type</a></span> <span class="id">t2</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="ergo_ctype_decl_from_expand">ergo_ctype_decl_from_expand</a></span> (<span class="id">ctxt</span> : <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#expand_ctxt">expand_ctxt</a></span>) : <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tbrand_context_decls">tbrand_context_decls</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html#map">List.map</a></span> (<span class="kwd">fun</span> <span class="id">xyz</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#fst">fst</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#xyz">xyz</a></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">rtl</span> := <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#snd">snd</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#snd">snd</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#xyz">xyz</a></span>) <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.trec">trec</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.open_kind">open_kind</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Bindings.html#rec_sort">rec_sort</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html#map">List.map</a></span> (<span class="kwd">fun</span> <span class="id">xy</span> =&gt; (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#fst">fst</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#xy">xy</a></span>, <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ergo_type_to_ergoc_type">ergo_type_to_ergoc_type</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#snd">snd</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#xy">xy</a></span>))) <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#rtl">rtl</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Bindings.html#rec_sort_sorted">rec_sort_sorted</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html#map">List.map</a></span> (<span class="kwd">fun</span> <span class="id">xy</span> =&gt; (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#fst">fst</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#xy">xy</a></span>, <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ergo_type_to_ergoc_type">ergo_type_to_ergoc_type</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#snd">snd</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#xy">xy</a></span>))) <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#rtl">rtl</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Bindings.html#rec_sort">rec_sort</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html#map">List.map</a></span> (<span class="kwd">fun</span> <span class="id">xy</span> =&gt; (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#fst">fst</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#xy">xy</a></span>, <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ergo_type_to_ergoc_type">ergo_type_to_ergoc_type</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#snd">snd</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#xy">xy</a></span>))) <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#rtl">rtl</a></span>))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Logic.html#eq_refl">eq_refl</a></span>))) <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ctxt">ctxt</a></span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">End</span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ErgoTypetoErgoCType.ErgoTypetoErgoCType">ErgoTypetoErgoCType</a></span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">Section</span> <span class="id"><a name="ErgoTypetoErgoCType.Translate">Translate</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Local</span> <span class="kwd">Open</span> <span class="kwd">Scope</span> <span class="id">string</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Import</span> <span class="id">ErgoCTypes</span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="brand_relation_maybe">brand_relation_maybe</a></span> <span class="id">hierarchy</span> : <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tbrand_relation">tbrand_relation</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;:= <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult_of_qresult">eresult_of_qresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span> (<span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.mk_tbrand_relation">mk_tbrand_relation</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#hierarchy">hierarchy</a></span>).<br/>
<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="mk_model_type_decls">mk_model_type_decls</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;{<span class="id">br</span>:<span class="id"><a href="https://querycert.github.io/html/Qcert.Common.Brands.BrandRelation.html#brand_relation">brand_relation</a></span>}<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">ctxt</span> : <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#expand_ctxt">expand_ctxt</a></span>) : <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tbrand_context_decls">tbrand_context_decls</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;@<span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ergo_ctype_decl_from_expand">ergo_ctype_decl_from_expand</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#br">br</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ctxt">ctxt</a></span>.<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="label_of_decl">label_of_decl</a></span> (<span class="id">decl</span>:<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#laergo_type_declaration">laergo_type_declaration</a></span>) : <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#decl">decl</a></span>.(<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#type_declaration_name">type_declaration_name</a></span>).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="name_of_decl">name_of_decl</a></span> : <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#laergo_type_declaration">laergo_type_declaration</a></span> -&gt; <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> := <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#label_of_decl">label_of_decl</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="decls_table">decls_table</a></span> (<span class="id">decls</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#laergo_type_declaration">laergo_type_declaration</a></span>) : <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> * <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#laergo_type_declaration">laergo_type_declaration</a></span>) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html#map">List.map</a></span> (<span class="kwd">fun</span> <span class="id">d</span> =&gt; (<span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#d">d</a></span>.(<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#type_declaration_name">type_declaration_name</a></span>), <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#d">d</a></span>)) <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#decls">decls</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="edge_of_decl">edge_of_decl</a></span> (<span class="id">dt</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string">string</a></span> * <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#laergo_type_declaration">laergo_type_declaration</a></span>)) (<span class="id">decl</span>:<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#laergo_type_declaration">laergo_type_declaration</a></span>) : <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#laergo_type_declaration">laergo_type_declaration</a></span> * <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#laergo_type_declaration">laergo_type_declaration</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">outedges</span> := <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#type_declaration_extend_rel">type_declaration_extend_rel</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#decl">decl</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#decl">decl</a></span>, <span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html#concat">List.concat</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html#map">List.map</a></span> (<span class="kwd">fun</span> <span class="id">xy</span> =&gt; <span class="kwd">match</span> <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Assoc.html#lookup">lookup</a></span> <span class="id"><a href="http://coq.inria.fr/library/Coq.Strings.String.html#string_dec">string_dec</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#dt">dt</a></span> (<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#snd">snd</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#xy">xy</a></span>) <span class="kwd">with</span> | <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#None">None</a></span> =&gt; <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span> | <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#Some">Some</a></span> <span class="id">x</span> =&gt; <span class="id">x</span> :: <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#nil">nil</a></span> <span class="kwd">end</span>) <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#outedges">outedges</a></span>)).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="graph_of_decls">graph_of_decls</a></span> (<span class="id">decls</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#laergo_type_declaration">laergo_type_declaration</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;: <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> (<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#laergo_type_declaration">laergo_type_declaration</a></span> * <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> (<span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#laergo_type_declaration">laergo_type_declaration</a></span>)) :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">dt</span> := <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#decls_table">decls_table</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#decls">decls</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="http://coq.inria.fr/library/Coq.Lists.List.html#map">map</a></span> (<span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#edge_of_decl">edge_of_decl</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#dt">dt</a></span>) <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#decls">decls</a></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="sort_decls">sort_decls</a></span> (<span class="id">decls</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#laergo_type_declaration">laergo_type_declaration</a></span>) : <span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#laergo_type_declaration">laergo_type_declaration</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Misc.html#coq_toposort">coq_toposort</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#label_of_decl">label_of_decl</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#name_of_decl">name_of_decl</a></span> (<span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#graph_of_decls">graph_of_decls</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#decls">decls</a></span>).<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="brand_model_of_declarations">brand_model_of_declarations</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">decls</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#laergo_type_declaration">laergo_type_declaration</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;: <span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult">eresult</a></span> <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tbrand_model">ErgoCTypes.tbrand_model</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">decls</span> := <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#sort_decls">sort_decls</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#decls">decls</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">ctxt</span> := <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ergo_expand_extends_in_declarations">ergo_expand_extends_in_declarations</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#decls">decls</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">let</span> <span class="id">hierarchy</span> := <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ergo_hierarchy_from_expand">ergo_hierarchy_from_expand</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ctxt">ctxt</a></span> <span class="kwd">in</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eolift">eolift</a></span> (<span class="kwd">fun</span> <span class="id">br</span> =&gt;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id"><a href="ErgoSpec.Common.Utils.Result.html#eresult_of_qresult">eresult_of_qresult</a></span> <span class="id"><a href="ErgoSpec.Common.Utils.Provenance.html#dummy_provenance">dummy_provenance</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.mk_tbrand_model">mk_tbrand_model</a></span> (@<span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#mk_model_type_decls">mk_model_type_decls</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#br">br</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ctxt">ctxt</a></span>)))<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#brand_relation_maybe">brand_relation_maybe</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#hierarchy">hierarchy</a></span>).<br/>
<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">Definition</span> <span class="id"><a name="force_brand_model_of_declarations">force_brand_model_of_declarations</a></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id">decls</span>:<span class="id"><a href="http://coq.inria.fr/library/Coq.Init.Datatypes.html#list">list</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoType.html#laergo_type_declaration">laergo_type_declaration</a></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;: <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tbrand_model">ErgoCTypes.tbrand_model</a></span> :=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">match</span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#brand_model_of_declarations">brand_model_of_declarations</a></span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#decls">decls</a></span> <span class="kwd">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Result.html#Success">Success</a></span> <span class="id">_</span> <span class="id">_</span> <span class="id">s</span> =&gt; <span class="id">s</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id"><a href="https://querycert.github.io/html/Qcert.Utils.Result.html#Failure">Failure</a></span> <span class="id">_</span> <span class="id">_</span> <span class="id">e</span> =&gt; <span class="id"><a href="ErgoSpec.Backend.ErgoBackend.html#ErgoCTypes.tempty_brand_model">tempty_brand_model</a></span> <br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="kwd">end</span>.<br/>
<br/>
&nbsp;&nbsp;<span class="kwd">End</span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ErgoTypetoErgoCType.Translate">Translate</a></span>.<br/>
<br/>
<span class="kwd">End</span> <span class="id"><a href="ErgoSpec.Common.Types.ErgoTypetoErgoCType.html#ErgoTypetoErgoCType">ErgoTypetoErgoCType</a></span>.<br/>

</div>
<div class="footer"><hr/>Generated by <a href="https://github.com/xavierleroy/coq2html/">coq2html</div>
</body>
</html>
